Nuprl Lemma : loc_wf
0,22
postcript
pdf
E
,
X1
,
X2
:Type,
info
:(
E
(Id
X1
+(IdLnk
E
)
X2
)),
e
:
E
. loc(
e
)
Id
latex
Definitions
loc(
e
)
,
ecase1(
e
;
info
;
i
.
f
(
i
);
l
,
e'
.
g
(
l
;
e'
))
,
x
.
t
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
destination(
l
)
,
x
:
A
.
B
(
x
)
,
Id
,
IdLnk
,
t
T
Lemmas
IdLnk
wf
,
Id
wf
,
ldst
wf
,
ecase1
wf
origin
E, X1, X2:Type, info:(E
(Id
X1+(IdLnkE)X2)), e:E. loc(e) 
Id E, X1, X2:Type, info:(E(IdX1+(IdLnkE)X2)), e:E. loc(e) Id 
x. t(x)x,y. t(x;y)x:A. B(x) T